Search for: All records

Symbolic execution is a powerful verification tool for hardware designs, in particular for security validation. However, symbolic execution suffers from the path explosion problem in which the number of paths to explore grows exponentially with the number of branches in the design. We introduce a new approach, piecewise composition, which leverages the modular structure of hardware to transfer the work of path exploration to SMT solvers. Piecewise composition works by recognizing that independent parts of a design can each be explored once, and the exploration reused. A hardware design with N independent always blocks and at most b branch points per block will require exploration of O((2^b)N) paths in a single clock cycle with our approach compared to O(2^(bN)) paths using traditional symbolic execution. We present Sylvia, a symbolic execution engine implementing piecewise composition. The engine operates directly over RTL without requiring translation to a netlist or software simulation. We evaluate our tool on multiple open-source SoC and CPU designs, including the OR1200 and PULPissimo RISC-V SoC. The piecewise composition technique reduces the number of paths explored by an order of magnitude and reduces the runtime by 97% compared to our baseline. Using 84 properties from the security literature we find assertion violations in open-source designs that traditional model checking and formal verification tools do not find. 

We present SEIF, an exploratory methodology for information flow verification based on symbolic execution. SEIF begins with a statically built overapproximation of the information flow through a design and uses guided symbolic execution to provide a more precise picture of how information flows from a given set of security critical signals. SEIF can recognize and eliminate non-flows with high precision and for the true flows can find the corresponding paths through the design state with high coverage. We evaluate SEIF on two open-source CPUs, an AES core, and the AKER access control module. SEIF can be used to find counterexamples to information flow properties, and also to explore all flows originating from a source signal of interest. SEIF accounts for 86–90% of statically identified possible flows in three open-source designs. SEIF’s search strategies enable exploring the designs for 10-12 clock cycles in 4-6 seconds on average, demonstrating that this new exploratory style of information flow analysis can be practical. 

Hardware security creates a hardware-based security foundation for secure and reliable operation of systems and applications used in our modern life. The presence of design for security, security assurance, and general security design life cycle practices in product life cycle of many large semiconductor design and manufacturing companies these days indicates that the importance of hardware security has been very well observed in industry. However, the high cost, time, and effort for building security into designs and assuring their security - due to using many manual processes - is still an important obstacle for economy of secure product development. This paper presents several promising directions for automation of design for security and security assurance practices to reduce the overall time and cost of secure product development. First, we present security verification challenges of SoCs, possible vulnerabilities that could be introduced inadvertently by tools mapping a design model in one level of abstraction to its lower level, and our solution to the problem by automatically mapping security properties from one level to its lower level incorporating techniques for extension and expansion of the properties. Then, we discuss the foundation necessary for further automation of formal security analysis of a design by incorporating threat model and common security vulnerabilities into an intermediate representation of a hardware model to be used to automatically determine if there is a chance for direct or indirect flow of information to compromise confidentiality or integrity of security assets. Finally, we discuss a pre-silicon-based framework for practical and time-and-cost effective power-side channel leakage analysis, root-causing the side-channel leakage by using the automatically generated leakage profile of circuit nodes, providing insight to mitigate the side-channel leakage by addressing the high leakage nodes, and assuring the effectiveness of the mitigation by reprofiling the leakage to prove its acceptable level of elimination. We hope that sharing these efforts and ideas with the security research community can accelerate the evolution of security-aware CAD tools targeted to design for security and security assurance to enrich the ecosystem to have tools from multiple vendors with more capabilities and higher performance. 

Isadora is a methodology for creating information flow specifications of hardware designs. The methodology combines information flow tracking and specification mining to produce a set of information flow properties that are suitable for use during the security validation process, and which support a better understanding of the security posture of the design. Isadora is fully automated; the user provides only the design under consideration and a testbench and need not supply a threat model nor security specifications. We evaluate Isadora on a RISC-V processor plus two designs related to SoC access control. Isadora generates security properties that align with those suggested by the Common Weakness Enumerations (CWEs), and in the case of the SoC designs, align with the properties written manually by security experts. 

Security specification mining is a relatively new line of research that aims to develop a set of security properties for use during the design validation phase of the hardware life-cycle. Prior work in this field has targeted open-source RISC architectures and relies on access to the register transfer level design, developers’ repositories, bug tracker databases, and email archives. We develop Astarte, a tool for security specification mining of closed source, CISC architectures. As with prior work, we target properties written at the instruction set architecture (ISA) level. We use a full-system fast emulator with a lightweight extension to generate trace data, and we partition the space of security properties on security-critical signals in the architecture to manage complexity. We evaluate the approach for the x86-64 ISA. The Astarte framework produces roughly 1300 properties. Our automated approach produces a categorization that aligns with prior manual efforts. We study two known security flaws in shipped x86/x86-64 processor implementations and show that our set of properties could have revealed the flaws. Our analysis provides insight into those properties that are guaranteed by the ISA, those that are required of the operating system, and those that have become de facto properties by virtue of many operating systems assuming the behavior. 

This paper presents Transys, a tool for translating security critical properties written for one hardware design to analogous properties suitable for a second design. Transys works in three passes adjusting the variable names, arithmetic expressions, logical preconditions, and timing constraints of the original property to retain the intended semantics of the property while making it valid for the second design. We evaluate Transys by translating 27 assertions written in a temporal logic and 9 properties written for use with gate level information flow tracking across 38 AES designs, 3 RSA designs, and 5 RISC processor designs. Transys successfully translates 96% of the properties. Among these, the translation of 23 (64%) of the properties achieved a semantic equivalence rate of above 60%. The average translation time per property is about 70 seconds. 

This paper presents UNDINE, a tool to automatically generate security critical Linear Temporal Logic (LTL) properties of processor architectures. UNDINE handles complex templates, such as those involving four or more variables, register equality to a constant, and terms written over register slices. We introduce the notion of event types, which allows us to reduce the complexity of the search for a given template. We build a library of nine typed property templates that capture the patterns that are common to security critical properties for RISC processors. We evaluate the performance and efficacy of UNDINE and our library of typed templates on the OR1200, Mor1kx, and RISC-V processors. 

This paper presents hardware-oriented symbolic execution that uses a recursive algorithm to find, and generate exploits for, vulnerabilities in hardware designs. We first define the problem and then develop and formalize our strategy. Our approach allows for a targeted search through a possibly infinite set of execution traces to find needle-in-a-haystack error states. We demonstrate the approach on the open-source OR1200 RISC processor. Using the presented method, we find, and generate exploits for, a control-flow bug, an instruction integrity bug and an exception related bug.